import Text.Printf
import Util.Object(newInt)
import Data.String.Utils(replace)
import Data.Char(toLower)
import Data.Dates


-- Options
--universal = False
optAllCode = False
optOptimizeHarmonyPred = True
optClosedHarmonyPred = True
optClosedPeakAndValeyPred = True

--
 
n = 2
m = 2

tolower = map toLower

makeVar :: Int -> String
makeVar i = "x"++show i 

newVar :: IO String
newVar = 
    do
      n <- newInt
      return (makeVar n)

substitute [] str = str
substitute ((pat,repl):xs) str = replace pat repl (substitute xs str)

join :: String -> [String] -> String
join sep [] = ""
join sep [x] = x
join sep (x:xs) = x ++ sep ++ join sep xs 

codeheader="var2 Tot;\n"
               ++"var1 N where N = max Tot;\n"
               ++"defaultwhere1(p) = p in Tot;\n"
               ++"defaultwhere2(P) = P sub Tot;\n"
               ++"var2 U;\n"

codesuccessor=
    "pred successor(var1 x, var1 y, var2 X) =\n" 
     ++"\tx < y\n" 
     ++"\t& {x,y} sub X\n"
     ++"\t& all1 z  where z in X: (z <= x |  y <= z);\n"

codesubdivision=
    "pred subdivision(var1 x, var1 y, var2 X) =\n"
     ++"\tx < y &\n" 
     ++"\tx in X &\n" 
     ++"\ty in X &\n"
     ++"\tall1 z : ((z in X) => (x < z & z < y));\n"

codeless=
    "pred less(var2 U, var1 x,var1 y,var1 z,var1 w) =\n"
     ++"\tx < y\n"
     ++"\t& z <= x\n"
     ++"\t& y <= w\n"
     ++"\t& (z < x => x notin U)\n"
     ++"\t& (y < w => y in U);\n"

codenorthUTot =
    "pred northUTot(var2 U, var2 Tot, var1 x,var1 y,var1 z,var1 w) =\n"
     ++"\tlet1 m = max {x,z} in\n"
     ++"\tlet1 M = min {y,w} in\n"
     ++"\tm < M\n" 
     ++"\t& less(U,m,M,x,y)\n"
     ++"\t& less(Tot\\U,m,M,z,w);\n"

codemacros=
    "macro lessU(var1 x,var1 y,var1 z,var1 w) = less(U,x,y,z,w);\n"
    ++"macro lessUC(var1 x,var1 y,var1 z,var1 w) = less(Tot\\U,x,y,z,w);\n"
    ++"macro isValleyU(var1 i, var1 j) = lessU(i,j,0,N);\n"
    ++"macro isPeakU(var1 i, var1 j) = lessUC(i,j,0,N);\n"

codesinger letterMaj i n =
    let
        letterMin = tolower letterMaj
        otherletter = if (letterMaj == "B") then "a" else "b"
        thisbasso = letterMaj ++ show i
        strings = map (\x -> thisbasso ++ otherletter ++show x ) [1..n]
                  ++[thisbasso++letterMin++show i]
    in
      "var2 " ++ join ", " ([thisbasso]++strings)  ++ ";\n"
      ++thisbasso++" sub "++join " union " strings++";\n"

codebasso i = codesinger "B" i m
codealto i = codesinger "A" i n


codePeakValley :: String -> Int -> String              
codePeakValley letter i =
         let 
             thissinger = letter++show i
             histone=thissinger++(tolower letter)++show i
             peakOrValley = if letter == "B" then "Peak" else "Valley"
             body = substitute 
                        [("%B1",thissinger),("%B1b1",histone),("%Peak",peakOrValley)]
                        "closed%Peak(%B1,%B1b1);"
         in
           body 

codepeak i = codePeakValley "B" i
codevalley j = codePeakValley "A" j

            
codeequal=
    "pred equal(var1 x, var1 y, var2 X, var2 Y, var2 Z, var2 W) =\n"
     ++"\t(x in X union Z)\n"
    ++"\t& (x in X <=> y in Y)\n" 
    ++"\t& (x in Z <=> y in W);\n"

codeHarmonyPred=
    "pred "++ 
     "harmonyPred(var1 x, var1 y,var1 z, var1 w, var2 A1, var2 B1, var2 A1a1, var2 A1b1, var2 B1b1, var2 B1a1)=\n"
    ++"\t(x in A1 & successor(x,y,A1) & z in B1 & successor(z,w,B1) & northUTot(U,Tot,x,y,z,w)) => equal(x,z,A1a1,B1a1,A1b1,B1b1);\n"

codeClosedHarmonyPred=
    "pred "
     ++"closedHarmonyPred(var2 A1, var2 B1, var2 A1a1, var2 A1b1, var2 B1b1, var2 B1a1)=\n"
     ++"\tall1 x,y,z,w: harmonyPred(x,y,z,w,A1,B1,A1a1,A1b1,B1b1,B1a1);\n"

codePeakPred=
    "pred "
    ++"peak(var1 x, var1 y,var2 B1, var2 B1b1) = \n"
    ++ "\t((x in B1 & successor(x,y,B1) & isPeakU(x,y)) => x in B1b1);\n"

codeClosedPeakPred=
    "pred "
    ++"closedPeak(var2 B1, var2 B1b1) = \n"
    ++ "\tall1 x,y: peak(x,y,B1, B1b1);\n"


codeValleyPred=
    "pred "
    ++"valley(var1 x, var1 y,var2 B1, var2 B1b1) = \n"
    ++ "\t((x in B1 & successor(x,y,B1) & isValleyU(x,y)) => x in B1b1);\n"

codeClosedValleyPred=
    "pred "
    ++"closedValley(var2 B1, var2 B1b1) = \n"
    ++ "\tall1 x,y: valley(x,y,B1, B1b1);\n"



codenorth :: (Int,Int) -> String
codenorth  (i,j) = 
    let
        thisbasso = "B"++show i
        bassotone=thisbasso++"b"++show i
        otherbassotone=thisbasso++"a"++show j
        thisalto = "A"++show j
        altotone=thisalto++"a"++show j
        otheraltotone=thisalto++"b"++show i
    in
      substitute
      [("%A1",thisalto),("%B1",thisbasso),
       ("%A1a1",altotone),("%A1b1",otheraltotone),
       ("%B1b1",bassotone),("%B1a1",otherbassotone)
      ]
    ("closedHarmonyPred(%A1,%B1,%A1a1,%A1b1,%B1b1,%B1a1)")


timestamp :: DateTime -> String 
timestamp dt = printf "# Automatically generated on %s at %s\n" (today::String) (now::String)
               where
                 today=printf "%02d/%02d/%4d" ((day dt)::Int) ((month dt)::Int) ((year dt)::Int) 
                 now=printf "%02dh%02d" ((hour dt)::Int) ((minute dt)::Int)

main = 
    do
      dt <- getCurrentDateTime
      putStrLn $ timestamp dt
      putStrLn codeheader
      putStrLn codesuccessor
      --  putStrLn codesubdivision
      putStrLn codeless
      putStrLn codenorthUTot
      putStrLn codemacros
      putStrLn codeequal
      --- put Peak and Valleys preds and their 1st order closures 
      putStrLn codePeakPred
      putStrLn codeValleyPred
      if optClosedPeakAndValeyPred then
          do
            putStrLn codeClosedPeakPred
            putStrLn codeClosedValleyPred
      else
          return ()
      ---
      --- put HarmonyPred and its 1st order closure  
      putStrLn codeHarmonyPred
      if optClosedHarmonyPred then
          putStrLn codeClosedHarmonyPred
      else
          return ()
      ---
      if optOptimizeHarmonyPred then
          do
            putStrLn $ codesinger "B" 1 1 
            putStrLn $ codesinger "A" 1 1
            putStrLn $ 
                     let
                         northFormulas=map codenorth [(i,j) | i <- [1], j<- [1]]
                     in
                       (join ";\n" northFormulas)++";"
      else
          return ()
      if optAllCode then
          do
            putStrLn $ concat (map codebasso [1..n])
            putStrLn $ concat (map codealto [1..m])
            putStrLn $ join "\n" (map codepeak [1..n])
            putStrLn $ join "\n" (map codevalley [1..m])
            putStrLn $ 
                     let
                         northFormulas=map codenorth [(i,j) | i <- [1..n], j<- [1..m]]
                     in
                       (join ";\n" northFormulas)++";"
      else
          return ()
        
